1. Field of the Invention
This invention pertains in general to searching and manipulating database information in order to identify database elements satisfying specified properties. The invention more particularly pertains to manipulating database information to represent and solve satisfiability and other types of logic problems such as those involved in microprocessor verification and testing.
2. Description of the Related Art
Most computer systems that manipulate large amounts of data store the data by using general patterns of which the individual data elements are instances. The last few years have seen extraordinary improvements in the effectiveness of general-purpose algorithms that manipulate these data, as represented by improvements in the performance of Boolean satisfiability engines. These techniques have been applied in a wide range of application domains such as generative planning, circuit layout, and microprocessor verification and testing.
As the application domains become more sophisticated, the amount of information manipulated by these systems grows. In many cases, this information is represented by the set of ground instances of a single universally quantified axiom, but a single axiom such as∀xyz.[a(x,y)^b(y,z)→c(x,z)]has d3 ground instances if d is the size of the domain from which x, y and z are taken. In most cases, the prior art has dealt with the difficulty of managing the large number of ground instances by increasing computer memory and by finding axiomatizations for which ground theories remain manageably sized. In general, memory and these types of axiomatizations are both scarce resources and a more natural solution is desired. There have been some attempts to manipulate quantified axioms directly, but these attempts have been restricted to axioms of a particular form and structure. What is needed is a general approach that is capable of utilizing whatever structure exists in the data describing the application domain in order to minimize the memory and reduce the dependency on axiomatizations.